|
In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005). The disjunction property is satisfied by a theory if, whenever a sentence ''A ∨ B'' is a theorem, then either ''A'' is a theorem, or ''B'' is a theorem. The existence property or witness property is satisfied by a theory if, whenever a sentence is a theorem, where ''A''(''x'') has no other free variables, then there is some term ''t'' such that the theory proves . == Related properties == Rathjen (2005) lists five properties that a theory may possess. These include the disjunction property (DP), the existence property (EP), and three additional properties: * The numerical existence property (NEP) states that if the theory proves , where φ has no other free variables, then the theory proves for some . Here is a term in representing the number ''n''. * Church's rule (CR) states that if the theory proves then there is a natural number ''e'' such that, letting be the computable function with index ''e'', the theory proves . * A variant of Church's rule, CR1, states that if the theory proves then there is a natural number ''e'' such that the theory proves is total and proves . These properties can only be directly expressed for theories that have the ability to quantify over natural numbers and, for CR1, quantify over functions from to . In practice, one may say that a theory has one of these properties if a definitional extension of the theory has the property stated above (Rathjen 2005). 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「disjunction and existence properties」の詳細全文を読む スポンサード リンク
|